The advancement of network technologies such as bluetooth and WiFi has promoted the development of the Internet of Things(IoT). IoT facilitates people's lives, but there are also serious security issues in it. Without secure access control, illegal access of IoT may bring losses to users in many aspects. Traditional access control methods usually rely on a trusted central node, which is not suitable for an IoT environment with nodes distributed. The blockchain technology and smart contracts provide a more effective solution for access control in IoT applications. However, it is difficult to ensure the correctness of smart contracts used for access control in IoT applications by using general test methods. To solve this problem, a method was proposed to formally verify the correctness of smart contracts for access control by using model checking tool Verds. In the method, the state transition system was used to define the semantics of the Solidity smart contract, the Computation Tree Logic(CTL) formula was used to describe the properties to be verified, and the smart contract interaction and user behavior were modelled to form the input model of Verds and the properties to be verified. And then Verds was used to verify whether the properties to be verified are correct. The core of this method is the translation from a subset of Solidity to the input model of Verds. Experimental results on two smart contracts for access control of IoT source show that the proposed method can be used to verify some typical scenarios and expected properties of access control contracts, thereby improving the reliability of smart contracts.

The traditional Convolutional Neural Network (CNN) cannot directly process point cloud data, and the point cloud data must be converted into a multi-view or voxelized grid, which leads to a complicated process and low point cloud recognition accuracy. Aiming at the problem, a new point cloud classification and segmentation network called Linked-Spider CNN was proposed. Firstly, the deep features of point cloud were extracted by adding more Spider convolution layers based on Spider CNN. Secondly, by introducing the idea of residual network, short links were added to every Spider convolution layer to form residual blocks. Thirdly, the output features of each layer of residual blocks were spliced and fused to form the point cloud features. Finally, the point cloud features were classified by three-layer fully connected layers or segmented by multiple convolution layers. The proposed network was compared with other networks such as PointNet, PointNet++ and Spider CNN on ModelNet40 and ShapeNet Parts datasets. The experimental results show that the proposed network can improve the classification accuracy and segmentation effect of point clouds, and it has faster convergence speed and stronger robustness.